A:Type, eq:EqDecider(A), B:(AType), P:(A), f:fpf(A; x.B(x)), x:A, v:B(x).
(<x, v>  fpf-vals(eq; P; f))
 guard((((fpf-dom(eq; x; f))  ((P(x))))  (v = fpf-ap(f; eq; x)))) 

latex

Definitions

t  T, x(s), x:A. B(x), x:AB(x), P  Q, ff, False, A, , (x  l), b, Type, prop{i:l}, b, x:A  B(x), P  Q, P  Q, Unit, left + right, tt, <a, b>, guard(T), sq_type(T), let x = a in b(x), fpf-ap(f; eq; x), fpf-dom(eq; x; f), fpf-vals(eq; P; f), fpf(A; a.B(a)), EqDecider(T), f(a), x. t(x), remove-repeats(eq; L), type List, s = t, deq-member(eq; x; L), sqequal(s; t), subtype(S; T), suptype(S; T), {x:A| B(x)} , tl(l), n - m, if a<b then c else d, i <z j, i z j, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , nth_tl(n;as), hd(l), l[i], n + m, rec-case(a) of [] => s | x::y => z.t(x;y;z), x.A(x), Y, ||as||, a < b, A  B, , , [], void, A c B, P  Q, P  Q, decidable(P), cons(car; cdr), filter(P; l), map(f; as), zip(as; bs), eqof(d), bor(p; q), t.1, t.2, True

Lemmas

true wf, subtype rel self, assert of bor, or functionality wrt iff, deq property, pi2 wf, pi1 wf, guard wf, bor wf, eqof wf, list-subtype, subtype rel list, cons member, decidable assert, nil member, decidable false, false wf, fpf wf, deq wf, bool sq, member-remove-repeats, btrue wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, bnot wf, not wf, assert wf, l member wf, deq-member wf, bool wf, bfalse wf, remove-repeats wf